E,X1,X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), pred?:(E(?E)),
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(e:E, l:IdLnk.
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(e':E
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:((e'':E. 
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:((rcv?(e''))
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (sender(e'') = e)
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (link(e'') = l)
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:( (((e'' = e')  e'' < e')
info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), p:(  (loc(e') = destination(l)  Id)))).
SWellFounded(pred!(e;e'))
 (e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 (e,e':E. (loc(e) = loc(e')  Id)  (pred?(e) = pred?(e'))  (e = e'))
 (r:E. 
 (rcv?(r))
  (index(dE; dL; pred?; info; p; r)
  ( int_seg(0; ||receives(dE; dL; pred?; info; p; sender(r); link(r))||))) 

latex

Definitions

lelt(i; j; k), rel_exp(T; R; n), rel_plus(T; R), guard(T), x f y, rel_star(T; R), P  Q, P  Q, eventlist(pred?; e), sends-bound(p; e; l), (x  l), A  B, False, ge(i; j), ||as||, eqof(d), l[i], int_seg(i; j), receives(dE; dL; pred?; info; p; e; l), index(dE; dL; pred?; info; p; r), subtype(S; T), rcv-from-on(dE; dL; info; e; l; r), , SWellFounded(R(x;y)), A c B, A, b, first(e), pred(e), EqDecider(T), x:A. B(x), sender(e), IdLnk, link(e), P  Q, P  Q, e < e', destination(l), x,y. t(x;y), pred!(e;e'), Id, loc(e), Unit, prop{i:l}, P  Q, rcv?(e), x:A. B(x), t  T

Lemmas

rcv? wf, assert wf, unit wf, loc wf, Id wf, pred wf, first wf, not wf, pred! wf, strongwellfounded wf, ldst wf, cless wf, link wf, sender wf, IdLnk wf, deq wf, nat wf, rcv-from-on wf, receives wf, int seg wf, select wf, eqof wf, length wf1, non neg length, mu-bound, l member wf, sends-bound wf, eventlist wf, member filter, member eventlist, sends-bound-property, rel star weakening, cless-eq-loc, rel exp wf, nat plus inc, strong-sends-bound-property, assert-rcv-from-on, le wf, deq property